Sensor network applications are expected to perform critical tasks unattendedly for a long period, thus it is important to verify their reliability and correctness. Currently common programming languages, e.g. NesC, and platforms, e.g. TinyOS, for sensor networks adopt the low-level programming style. Although such designs are able to provide fine-grained control over the underlying resource constraints, they are difficult for human to comprehend, maintain, debug and verify sensor network applications.

PAT is developed to apply model checking techniques to the sensor network domain by this NesC module. The NesC module of PAT is created to automatically analyze behaviors and verify properties of TinyOS applications implemented in NesC. NesC programs are parsed to LTS semantic models, upon which the behaviors of TinyOS applications are analyzed and their properties are verified. The tool can assist program developers to analyze, simulate and verify their code, consequently improving the correctness and reliability of sensor network applications.

Currently, the implementation of NesC module follows the language features of NesC, and the execution model of TinyOS model, which are presented in the book TinyOS Programming by Philip Levis. Most syntax of the NesC language is supported now. Our approach is to generate Label Transition System (LTS) from nesC source code, and then explore the state space of the LTS to verify whether it satisfies certain properties.

Important notice: NesC module only supports application of TinyOS 2.x.

PAT is extended with this NesC module to automatically generate LTS semantic model from NesC programs, with a graphical behavior analysis interface (Simultor) and an interface for verifying various properties (Model Checker). The following figure shows the architecture of the NesC module in PAT.

Firstly, NesC source code is input to the NesC Process Generator, which generates NesC processes, with supports from the static NesC process library of TinyOS components; secondly, LTS Generator produces the corresponding LTS model; finally, execution traces of the resultant LTS are displayed via the simulator, and its the state space is explored by model checking algorithms to verify user-specified properties via the model checker.